\begin{tabbing}
$\forall$\=$M$:MsgA, $k$:Knd, $l$:IdLnk, $s$:$M$.state, $v$:$M$.V($k$), $i$:Id,\+
\\[0ex]${\it ms}$:((${\it tg}$:Id $\times$ if source($l$) = $i$ then $M$.da(rcv($l$,${\it tg}$)) else Top fi ) List).
\-\\[0ex]$M$.send($k$;$l$;$s$;$v$;${\it ms}$;$i$) $\in$ $\mathbb{P}$
\end{tabbing}